# -*- mode: snippet -*-
# name: J D d where
# key: J
# expand-env: ((yas-indent-line 'fixed))
# --
J D d where
  D : (y : ?) → ? ≡ ? → Type ?
  D y p = ?
  d : D ? refl
  d = ?